@Book{Andrews,
  author = 	 {Peter B. Andrews},
  ALTeditor = 	 {},
  title = 	 {An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof},
  publisher = 	 {Academic Press},
  year = 	 {1986},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  series = 	 {Computer Science and Applied Mathematics Series},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{Camilleri-et-al,
  author = 	 {A. J. Camilleri and T. F. Melham and M. J. C. Gordon},
  title = 	 {Hardware Verification using Higher-Order Logic},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {From {HDL} Descriptions to Guaranteed Correct Circuit Designs: Proceedings of the {IFIP} {WG} 10.2 Working Conference},
  pages = 	 {43--67},
  year = 	 {1987},
  editor = 	 {D. Borrione},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  address = 	 {Grenoble},
  month =        sep,
  OPTorganization = {},
  publisher = {North-Holland},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Article{Church,
  author = 	 {Alonzo Church},
  title = 	 {A Formulation of the Simple Theory of Types},
  journal = 	 {Journal of Symbolic Logic},
  year = 	 {1940},
  OPTkey = 	 {},
  volume = 	 {5},
  OPTnumber = 	 {},
  pages = 	 {56--68},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{coquand,
  author = 	 {T. Coquand},
  title = 	 {An Analysis of {G}irard's Paradox},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {Proceedings of the {ACM} Conference on {L}ogic in {C}omputer {S}cience},
  OPTpages = 	 {},
  year = 	 {1986},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  address = 	 {Boston},
  month =        jun,
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}



@Book{ml-handbook,
  author = 	 {G. Cousineau and M. Gordon and G. Huet and R. Milner and L. Paulson and C. Wadsworth},
  ALTeditor = 	 {},
  title = 	 {The {ML} Handbook},
  publisher = 	 {INRIA},
  year = 	 {1986},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InCollection{goguen,
  author = 	 {J. A. Goguen and J. W. Thatcher, and E. G. Wagner},
  title = 	 {An initial algebra approach to the specification, correctness, and implementation of abstract data types},
  booktitle = 	 {Current Trends in Programming Methodology},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {80--149},
  OPTpublisher = {Prentice-Hall},
  OPTyear = 	 {1978},
  OPTeditor = 	 {R. T. Yeh},
  OPTvolume = 	 {IV},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTtype = 	 {},
  OPTchapter = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}



@TechReport{HOL-paper,
  author = 	 {M. Gordon},
  title = 	 {{HOL}: A Machine Oriented Formulation of Higher-Order Logic},
  institution =  {University of Cambridge Computer Laboratory},
  year = 	 {1985},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number = 	 {68},
  OPTaddress = 	 {},
  month =        jul,
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{Why-HOL-paper,
  author = 	 {M. Gordon},
  title = 	 {Why higher-order Logic is a good formalism for specifying and verifying hardware},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {Formal Aspects of {VLSI} Design: Proceedings of the 1985 {E}dinburgh Workshop on {VLSI}},
  pages = 	 {153--177},
  year = 	 {1986},
  editor = 	 {G. Milne and P. A. Subrahmanyam},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher = {North-Holland},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Book{Edinburgh-LCF,
  author = 	 {M. Gordon and R. Milner and C. P. Wadsworth},
  ALTeditor = 	 {},
  title = 	 {Edinburgh {LCF}: A Mechanised Logic of Computation},
  publisher = 	 {Springer-Verlag},
  year = 	 {1979},
  OPTkey = 	 {},
  volume = 	 {78},
  OPTnumber = 	 {},
  series = 	 {Lecture Notes in Computer Science},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{Hanna-Daeche,
  author = 	 {F. K. Hanna and N. Daeche},
  title = 	 {Specification and Verification using Higher-Order Logic: A Case Study},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {Formal Aspects of {VLSI} Design: Proceedings of the 1985 {E}dinburgh Workshop on {VLSI}},
  pages = 	 {179--213},
  year = 	 {1986},
  editor = 	 {G. Milne and P. A. Subrahmanyam},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher = {North-Holland},
  OPTnote = 	 {},
  OPTannote = 	 {}
}


@Book{jrh:thesis,
  author = 	 {John Harrison},
  ALTeditor = 	 {},
  title = 	 {Theorem-proving with the Real Numbers},
  publisher = 	 {Springer},
  year = 	 {1998},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  series = 	 {{CPHC}/{BCS} Distinguished Dissertations},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}



@PhdThesis{hurd-thesis,
  author = 	 {Joe Hurd},
  title = 	 {Formal Verification of Probabilistic Algorithms},
  school = 	 {University of Cambridge},
  year = 	 {2002},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Book{Leisenring,
  author = 	 {A. C. Leisenring},
  ALTeditor = 	 {},
  title = 	 {Mathematical Logic and Hilbert's $\epsilon$-Symbol},
  publisher = 	 {Macdonald \& Co.~ Ltd.},
  year = 	 {1969},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  series = 	 {University Mathematical Series},
  address = 	 {London},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Book{MW,
  author = 	 {Zohar Manna and Richard Waldinger},
  ALTeditor = 	 {},
  title = 	 {The Logical Basis for Computer Programming},
  publisher = 	 {Addison-Wesley},
  year = 	 {1985},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}



@InCollection{Melham-banff,
  author = 	 {T. F. Melham},
  title = 	 {Automating Recursive Type Definitions in Higher Order Logic},
  booktitle = 	 {Current Trends in Hardware Verification and Automated Theorem Proving},
  OPTcrossref =  {},
  OPTkey = 	 {},
  pages = 	 {341--386},
  publisher = {Springer-Verlag},
  year = 	 {1989},
  editor = 	 {G. Birtwistle and P. A. Subrahmanyam},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTtype = 	 {},
  OPTchapter = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Book{sml,
  author = 	 {R. Milner and M. Tofte and R. Harper},
  ALTeditor = 	 {},
  title = 	 {The Definition of {S}tandard {ML}},
  publisher = 	 {MIT Press},
  year = 	 {1990},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Article{lcp-rewrite,
  author = 	 {L. Paulson},
  title = 	 {A Higher-Order Implementation of Rewriting},
  journal = 	 {Science of Computer Programming},
  year = 	 {1983},
  OPTkey = 	 {},
  volume = 	 {3},
  OPTnumber = 	 {},
  pages = 	 {119--149},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}


@Book{new-LCF-man,
  author = 	 {L. Paulson},
  ALTeditor = 	 {},
  title = 	 {Logic and Computation: Interactive Proof with {C}ambridge {LCF}},
  publisher = 	 {Cambridge University Press},
  year = 	 {1987},
  OPTkey = 	 {},
  volume = 	 {2},
  OPTnumber = 	 {},
  series = 	 {Cambridge Tracts in Theoretical Computer Science},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@TechReport{Stefan,
  author = 	 {S. Soko\l owski},
  title = 	 {A Note on Tactics in {\LCF}},
  institution =  {University of {E}dinburgh Department of Computer Science},
  year = 	 {1983},
  OPTkey = 	 {},
  OPTtype = 	 {},
  number = 	 {CSR-140-83},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Book{Z,
  author = 	 {M. Spivey},
  ALTeditor = 	 {},
  title = 	 {The {Z} Notation},
  publisher = 	 {Prentice-Hall},
  year = 	 {1989},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{wong,
  author = 	 {Wai Wong},
  title = 	 {Modelling bit vectors in {HOL}: The word library},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {Higher Order Logic Theorem Proving and its Applications, {HUG} '93},
  pages = 	 {371--384},
  year = 	 {1994},
  editor = 	 {Jeffrey J. Joyce and Carl-Johan H. Seger},
  volume = 	 {780},
  OPTnumber = 	 {},
  series = 	 {Lecture Notes in Computer Science},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher = {Springer-Verlag},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

% following is from HolBdd.bib

@string{JSC="Journal of Symbolic Computation"}

@incollection{Amarel,
  author      = "Saul Amarel",
  title       = "On representation of problems of reasoning about action",
  pages       = "131-171",
  booktitle   = "Machine Intelligence 3",
  editor      = "Donald Michie",
  publisher   = "Edinburgh University Press",
  year        = "1971"}

@inproceedings{CoudertBerthetMadre,
  editor	= "J. Sifakis",
  author        = "Olivier Coudert and Christian Berthet and Jean Christophe Madre",
  title		= "Verification of synchronous sequential machines
                   based on symbolic execution",
  booktitle	= "Automatic Verification Methods for Finite State Systems",
  year		= 1989,
  publisher	= "Springer-Verlag",
  pages         = {365-373},
  number        = "407",
  series	= {Lecture Notes in Computer Science}}


@Book{charniak80,
  author        = {E. Charniak and C. K. Riesbeck and D. V. McDermott},
  title         = {Artificial Intelligence Programming},
  publisher     = {Lawrence Erlbaum Associates},
  year          = 1980}


@mastersthesis{WingSangLee,
  author      = "Lee, Wing Sang",
  title       = "{ST} to {FL} translation for hardware design verification",
  school      = {The University of British Columbia},
  month       = apr,
  year        = "1994"}

@techreport{LeeGreenstreetSeger,
  author      = "Trevor W. S. Lee and Mark R. Greenstreet and Carl-Johan Seger",
  title       = "Automatic Verification of Asynchronous Circuits",
  institution = {The University of British Columbia},
  number      = {UBC TR~93-40},
  month       = nov,
  year        = "1993"}

@inproceedings{aagaard-iccad-95,
 author  = {Aagaard, Mark D. and Seger, Carl-Johan H.},
 title   = {The Formal Verification of a
            Pipelined Double-Precision {IEEE} Floating-Point
            Multiplier},
 booktitle = iccad,
 pages     = {7-10},
 year      = 1995,
 month     = nov,
 publisher = ieee-computer-society,
}

@incollection{hazelhurst-kropfbook-97,
 author    = {Hazelhurst, Scott and Seger, Carl-Johan H.},
 title     = {Symbolic Trajectory Evaluation},
 booktitle = {Formal Hardware Verification},
 publisher = {Springer-Verlag},
 year      = 1997,
 chapter   = 1,
 pages     = {3-78},
 editor    = {Kropf, Thomas},
}


@TECHREPORT{harrison-style,
        author          = "John Harrison",
        title           = "Floating point verification in {HOL} {L}ight:
                           the exponential function",
        institution     = "University of Cambridge Computer Laboratory",
        address         = "New Museums Site, Pembroke Street,
                           Cambridge, CB2 3QG, UK",
        year            = 1997,
        type            = "Technical Report",
        number          = 428,
        note            = "Available on the Web as
                           {\url{http://www.cl.cam.ac.uk/users/jrh/papers/tang.html}}"}

@Article{oleary-itj-99,
  author  = {O'Leary, John and Zhao, Xudong and Gerth, Robert and
             Seger, Carl-Johan H.},
  title   = {Formally Verifying {IEEE} Compliance of Floating-Point
             Hardware},
  journal = {Intel Technology Journal},
  year    = 1999,
  month   = {First Quarter},
  note    = {Online at {\url{http://developer.intel.com/technology/itj/}}}
}

@techreport{SegerVoss,
  author      = "Carl-Johan H. Seger",
  title       = {Voss - A Formal Hardware Verification System: User's Guide},
  institution = {The University of British Columbia},
  number      = {UBC TR~93-45},
  month       = dec,
  year        = "1993"}


@techreport{McMillan99,
  author      = "K. L. McMillan",
  title       = {A methodology for hardware verification using compositional model checking},
  institution = {Cadence Berkeley Labs},
  month       = apr,
  note        = {Available at {\url{http://www-cad.eecs.berkeley.edu/~kenmcmil/}}},
  year        = "1999"}


@INPROCEEDINGS{aagaard-tphols-99,
  AUTHOR = {Aagaard, Mark D. and Jones, Robert B. and Seger, Carl-Johan H.},
  TITLE = "{Lifted-FL: A Pragmatic Implementation of Combined Model
             Checking and Theorem Proving}",
  BOOKTITLE = {Theorem Proving in Higher Order Logics (TPHOLs99)},
  YEAR = {1999},
  publisher	= "Springer-Verlag",
  pages         = {323-340},
  number        = "1690",
  series	= {Lecture Notes in Computer Science},
}



@inproceedings{aagaard-dac-98,
 author    = {Aagaard, Mark D. and Jones, Robert B. and Seger, Carl-Johan
 H.},
 title     = {Combining Theorem Proving and Trajectory Evaluation
              in an Industrial Environment},
 booktitle = {Design Automation Conference (DAC)},
 year      = 1998,
 month     = jul,
 pages     = {538-541},
 organization = {ACM/IEEE},
}

@techreport{ButlerAutopilot,
  author      = "Ricky W. Butler",
  title       = "An Introduction to Requirements
                 Capture using {PVS}: Specification of a Simple Autopilot",
  institution = {NASA},
  number      = {TR 110255},
  month       = may,
  year        = "1996"}

@techreport{YoungAutopilot,
  author      = "William D. Young",
  title       = "The Specification of a Simple Autopilot in {ACL2}",
  institution = {Computational Logic Inc},
  number      = {CLI Internal Note \#327},
  month       = jul,
  year        = "1996"}

@misc{HoareFest,
  author      = "Mike Gordon",
  title       = {Programming combinations of deduction and {BDD}-based symbolic calculation},
  note        = {Draft available at
                 {\url{http://www.cl.cam.ac.uk/~mjcg/celebration/}}}
}



@misc{GordonVerilogSemantics,
  author      = "Mike Gordon",
  title       = {Synthesizable Verilog: syntax and semantics},
  note        = {Draft available at
                 {\url{http://www.cl.cam.ac.uk/users/mjcg/Verilog/V/V.ps.gz}}}
}

@incollection{JoyceSeger,
  author	= "J. Joyce and C. Seger",
  title		= "{The HOL-Voss System: Model-Checking
                    inside a General-Purpose Theorem-Prover}",
  booktitle     = {Higher Order Logic
                    Theorem Proving and its Applications: 6th International
                    Workshop, HUG'93, Vancouver, B.C., August 11-13 1993},
  editor        = {J. J. Joyce and C.-J. H. Seger},
  year		= 1994,
  publisher     = "Spinger-Verlag",
  pages         = {185-198},
  volume        = "780",
  series        = {Lecture Notes in Computer Science}
}

@misc{HenrikNotes,
  author	= "Henrik Reif Andersen",
  title		= "{An Introduction to Binary Decision Diagrams}",
  year		= 1997,
  month         = oct,
  organization  ="Department of Information Technology, Technical University of Denmark,
                  Building 344, DK-2800 Lyngby, Denmark",
  note          ="Lecture notes for 49285 Advanced Algorithms E97.
                  Available from: {\url{http://www.it.dtu.dk/~hra}}"
}


@misc{PaulsonMiniscoping,
  key           = "Paulson",
  note          = {Larry Paulson, private communication.}
}

@book{EdinLCF,
  author = {M. J. C. Gordon and  R. Milner and C. P. Wadsworth},
  title = {{Edinburgh LCF}: A Mechanised Logic of Computation},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = 78,
  year = 1979
}



@book{McMillanBook,
  author = {Kenneth L. McMillan},
  title = {Symbolic Model Checking},
  publisher = {Kluwer Academic Publishers},
  year = 1993
}



@book{ClarkeBook,
  author = {Edmund M. Clarke Jr. and Orna Grumberg},
  title = {Model Checking},
  publisher = {The MIT Press},
  year = 1999
}


@misc{PVS,
  key = "PVS",
  note = {See web page {\url{http://www.csl.sri.com/pvs.html}}}
}


@misc{Prosper,
  key = "Prosper",
  note = {See web page {\url{http://www.dcs.gla.ac.uk/prosper/}}}
}



@misc{BuDDy,
  key = "Lind",
  note = {J{\o}rn Lind-Nielsen's BuDDy
          package is documented at {\url{http://www.itu.dk/research/buddy/}}}
}

@inproceedings{Rajan95:CAV,
        TITLE = {An Integration of Model-Checking with Automated Proof
                Checking},
        AUTHOR = {S. Rajan and N. Shankar and M. K. Srivas},
        BOOKTITLE = {Computer-Aided Verification, CAV '95},
        EDITOR = {Pierre Wolper},
        PAGES = {84--97},
        PUBLISHER = {Springer-Verlag},
        SERIES = {Lecture Notes in Computer Science},
        VOLUME = 939,
        MONTH = jun,
        YEAR = 1995,
        ADDRESS = {Liege, Belgium}
}

@InCollection{basin98:_combin_ws1s_hol,
  author =       {Basin, David and Friedrich, Stefan},
  title =        {Combining {WS1S} and {HOL}},
  booktitle =    {Frontiers of Combining Systems, Second International
                  Workshop, Amsterdam, September 1998},
  publisher =    {Kluwer Academic Publishers},
  year =         1998,
  series =       {Applied Logic Series},
  note =         {To appear}
}

@techreport{Butler96:rqts,
        TITLE = {An Introduction to Requirements Capture Using {PVS}:
                Specification of a Simple Autopilot},
        AUTHOR = {Ricky W. Butler},
        TYPE = {NASA Technical Memorandum},
        NUMBER = 110255,
        MONTH = may,
        YEAR = 1996,
        INSTITUTION = {NASA Langley Research Center},
        ADDRESS = {Hampton, VA}
}



@article{Milner-types,
 author = {R. Milner},
 title = {A Theory of Type Polymorphism in Programming},
 journal = {Journal of Computer and System Sciences},
 volume = {17},
 number = {3},
 pages = {348-375},
 month = dec,
 year = {1978}
}


@incollection{BoyerMooreLinearArith,
  author      = "R. S. Boyer and J Moore",
  title       = "Integrating Decision Procedures into Heuristic Theorem Provers:
                 A Case Study of Linear Arithmetic",
  pages       = "83-124",
  booktitle   = "Machine Intelligence 11",
  publisher   = "Oxford University Press",
  year        = "1988"}

@article{BryantSurvey,
 author = {Randall E. Bryant},
 title = {Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams},
 journal = {ACM Computing Surveys},
 volume = {24},
 number = {3},
 pages = {293-318},
 month = sep,
 year = {1992}
}

@PhDThesis{RJBPhDThesis,
   author = "R. J. Boulton",
   title = "Efficiency in a Fully-Expansive Theorem Prover",
   school = "University of Cambridge Computer Laboratory",
   year = "1994",
   address = "New Museums Site, Pembroke Street, Cambridge CB2 3QG, U.K.",
   month = may,
   note = "Technical Report 337."}

@techreport{boulton92b,
 author = {R. J. Boulton},
 title = {On efficiency in theorem provers which fully expand proofs into
          primitive inferences},
 institution = {University of Cambridge Computer Laboratory},
 year = {1992},
 month = feb,
 number = {248},
 note = {This report is based on Richard Boulton's PhD thesis.}
}

@techreport{mjcg99a,
 author = {Mike Gordon},
 title = {Programming combinations of deduction and {BDD}-based
          symbolic calculation },
 institution = {University of Cambridge Computer Laboratory},
 year = {1999},
 month = dec,
 number = {480},
}

@techreport{GordonLarsen,
 author = {Mike Gordon and Ken Friis Larsen},
 title = {Combining the {Hol98} Proof Assistant with
          the {BuDDy} {BDD} package},
 institution = {University of Cambridge Computer Laboratory},
 year = {1999},
 month = dec,
 number = {481},
}

@book{GordonMelham,
 editor = {M. J. C. Gordon and T. F. Melham},
 title = {Introduction to HOL:
          a theorem-proving environment for higher-order logic},
 publisher = {Cambridge University Press},
 year = {1993}
}

@book{MelhamBook,
  editor = {T. F. Melham},
  title = {Higher Order Logic and Hardware Verification},
  publisher = {Cambridge University Press},
  series = {Cambridge Tracts in Theoretical Computer Science 31},
  year = 1993
}


@InCollection{WhyHOL,
  author        = "Mike Gordon",
  editor        = "G. Milne and P. A. Subrahmanyam",
  title         = "Why higher-order logic is a good formalism for specifying
                   and verifying hardware",
  booktitle     = "Formal Aspects of VLSI Design",
  pages         = "153--177",
  publisher     = "North-Holland",
  year          = 1986}


@InProceedings{SemanticChallenge,
 Author = "Mike Gordon",
 title  = "The Semantic Challenge of {Verilog} {HDL}",
 booktitle = "Tenth Annual IEEE Symposium on Logic in Computer Science",
 place = "San Diago, California, USA",
 dates = "26--29 June",
 publisher = "{IEEE Computer Society Press}",
 year = "1995",
 pages = "136--145",
}

@INPROCEEDINGS{tphols2000-Gordon,
        editor          = "J. Harrison and M. Aagaard",
        booktitle       = "Theorem Proving in Higher Order Logics:
                           13th International Conference, TPHOLs 2000",
        series          = "Lecture Notes in Computer Science",
        volume          = 1869,
        year            = 2000,
        publisher       = "Springer-Verlag",
        title           = "Reachability programming in {HOL} using {BDD}s",
        author          = "Michael J. C. Gordon",
        pages           = "180--197"}

@InProceedings{Gordon:TPHOLs2000,
        editor          = "J. Harrison and M. Aagaard",
        booktitle       = "Theorem Proving in Higher Order Logics:
                           13th International Conference, TPHOLs 2000",
        series          = "Lecture Notes in Computer Science",
        volume          = 1869,
        year            = 2000,
        publisher       = "Springer-Verlag",
        title           = "Reachability programming in {HOL} using {BDD}s",
        author          = "Michael J. C. Gordon",
        pages           = "180--197"}

@misc{Amjad:TPHOLs2001,
 Author = "Hasan Amjad",
 title  = "{BDD} Representation Judgements in {HOL}: A Performance Evaluation",
 note = "Category B paper presented at the
         {\it 14th International Conference on Theorem Proving and Higher Order Logics\/}.
         Edinburgh, Scotland, UK, August 2001.
         Available from \url{http://www.cl.cam.ac.uk/~ha227/}",
}



@Book{Isabelle-book,
  author        = "Lawrence C. Paulson",
  title         = "Isabelle: A Generic Theorem Prover",
  publisher     = "Springer-Verlag",
  year          = 1994,
  volume        = "828",
  series        = {Lecture Notes in Computer Science}}

@Article{paulson-jcs,
  author =       {Lawrence C. Paulson},
  title =        {The Inductive Approach to Verifying Cryptographic Protocols},
  journal =      {Journal of Computer Security},
  year =         1998,
  volume        = 6,
  pages         = {85-128}}




@Book{Back,
  author        = "Ralph-Johan Back and Joakim von Wright",
  title         = "Refinement Calculus: A Systematic Introduction",
  publisher     = "Springer-Verlag",
  year          = 1998,
  series        = {Graduate Texts in Computer Science}}


@Book{Morgan,
  author =       {Carroll Morgan},
  title         = "Refinement Calculus: A Systematic Introduction",
  publisher     = "Prentice Hall",
  year          = 1990,
  series        = {Prentice Hall International Series in Computer Science}}

@InCollection{Hanna,
  author =       {F. K. Hanna and M Longley and N Daeche},
  editor =       {L. J. M. Claesen},
  title =        {Formal synthesis of digital systems},
  booktitle =    {Applied formal methods for correct VLSI design},
  publisher =    {North-Holland},
  year =         1989,
  pages =        "153--169"
}

@inproceedings{Fourman,
  author = "Finn, S. and Fourman, M. P. and Francis, M. and Harris, R.",
  title = "Formal System Design ---
    Interactive Synthesis based on Computer-Assisted Formal Reasoning",
  editor = "Claesen, L.",
  booktitle = "Formal VLSI Specification and Synthesis",
  publisher = "Elsevier",
  year = 1990
  }


@InProceedings{Curzon91,
  author =      "Paul Curzon",
  title =       "A Verified Compiler for a Structured Assembly Language",
  booktitle =   "Proceedings of the 1991 International Workshop on the {HOL}
                 Theorem Proving System and its Applications",
  year =        "1992",
  editor =       "Myla Archer and Jeffrey J. Joyce and Karl N. Levitt and
                 Phillip J. Windley",
  publisher =   "{IEEE} Computer Society Press",
}

@PhdThesis{slind-thesis,
  author = 	 {Konrad Slind},
  title = 	 {Reasoning about Terminating Functional Programs},
  school = 	 {Technical University of Munich},
  year = 	 {1999},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@inproceedings{Maranget2008,
  author = {Maranget, Luc},
  title = {Compiling Pattern Matching to Good Decision Trees},
  booktitle = {Proceedings of the 2008 ACM SIGPLAN Workshop on ML},
  series = {ML '08},
  year = {2008},
  isbn = {978-1-60558-062-3},
  location = {Victoria, BC, Canada},
  pages = {35--46},
  numpages = {12},
  url = {http://doi.acm.org/10.1145/1411304.1411311},
  doi = {10.1145/1411304.1411311},
  acmid = {1411311},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {decision trees, heuristics, match compilers},
}
